FDL - Nuprl Definition : prime_ideal

Nuprl Definition : prime_ideal_p

13,42

IsPrimeIdeal(R;P) == (

(P(1))) & (

a, b:|R|. (P(a * b))

((P(a))

(P(b))))

clarification:

IsPrimeIdeal(R;P) == (

(P(1R))) & (

a:|R|, b:|R|. (P(a (*R) b))

((P(a))

(P(b))))

Up rings 1

Wellformedness Lemmas prime ideal p wf

Definitions P & Q, A, 1, x:A. B(x), |r|, P Q, x f y, *, P Q